\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}_{1}$,${\it ds}_{2}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $x$,$y$:Id, $T_{1}$,$T_{2}$:Type,\+
\\[0ex]${\it ks}_{1}$,${\it ks}_{2}$:(Knd List), ${\it tr}_{1}$:(\=$k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}_{1}$)\} $\rightarrow$decl{-}state(${\it ds}_{1}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$$T_{1}$$\rightarrow$\+
\\[0ex]$T_{1}$),
\-\\[0ex]${\it tr}_{2}$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}_{2}$)\} $\rightarrow$decl{-}state(${\it ds}_{2}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$$T_{2}$$\rightarrow$$T_{2}$).
\-\\[0ex]($\neg$($x$ = $y$))
\\[0ex]$\Rightarrow$ fpf{-}compatible(Id; $a$.Type; id{-}deq; ${\it ds}_{1}$; fpf{-}single($x$; $T_{1}$))
\\[0ex]$\Rightarrow$ fpf{-}compatible(Id; $a$.Type; id{-}deq; ${\it ds}_{2}$; fpf{-}single($y$; $T_{2}$))
\\[0ex]$\Rightarrow$ fpf{-}compatible(Id; $x$.Type; id{-}deq; ${\it ds}_{2}$; fpf{-}join(id{-}deq; ${\it ds}_{1}$; fpf{-}single($x$; $T_{1}$)))
\\[0ex]$\Rightarrow$ fpf{-}compatible(Id; $x$.Type; id{-}deq; ${\it ds}_{1}$; fpf{-}join(id{-}deq; ${\it ds}_{2}$; fpf{-}single($y$; $T_{2}$)))
\\[0ex]$\Rightarrow$ R{-}compat\=\{i:l\}\+
\\[0ex](\=R{-}state{-}var($i$; ${\it ds}_{1}$; ${\it da}$; $x$; $T_{1}$; ${\it ks}_{1}$; ${\it tr}_{1}$);\+
\\[0ex]R{-}state{-}var($i$; ${\it ds}_{2}$; ${\it da}$; $y$; $T_{2}$; ${\it ks}_{2}$; ${\it tr}_{2}$))
\-\-
\end{tabbing}